?[$x$] $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case $x$ of inl($y$) =$>$ [$y$ / []] $\mid$ inr($y$) =$>$ []